T:Type, P:(T).
(x:T. Dec(P(x)))
 (L:(T List). X,Y:T List. (L = (X @ Y) & (xX. P(x)) & ((||Y||  1 )  P(hd(Y))))) 

latex

Definitions	type List, x:AB(x), s = t, f(a), x(s), A, x. t(x), xL. P(x), i  j , P  Q, x:A  B(x), P & Q, x:A. B(x), x:A. B(x), Dec(P), Type, , t  T, hd(l), #$n, ||as||, A  B, left + right, P  Q, <a, b>, , A c B, False, a < b, (x  l), , {x:A| B(x)} , l[i], {T}, s ~ t, , SQType(T), Void, [], x.A(x), as @ bs, n+m, A List, [car / cdr], P  Q, P  Q
Lemmas	l all cons, append wf, l all wf2, l member wf, false wf, guard wf, length wf1, hd wf, decidable wf, ge wf, not wf, l all wf